COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	proofs[f81,jmc]		generalized proofs
C00006 ENDMK
C⊗;
proofs[f81,jmc]		generalized proofs

	1981 Dec 5

	The following ideas are based on a conversation with
Carolyn Talcott.

	We generalize the notion of proof-checker as follows:

	1. A proof-checker  PC(s,y)  is computable total predicate
that takes a sentence  s  in a
certain language  L  and another data object  y.
If PC(s,y) is true,
then  s  is a theorem of the language  L.

	2. A bounded proof-checker is a function  BPC(s,y,t,m)
that carries out a process like that of  PC(s,y) but refuses
to to take more than time  t  or to user more than memory  m.  If
either bound is exceeded, then  BPC(s,y,t,m)
considers   s  as unproved.

	3. One simple kind of   PC  interprets  y  as a program that
generates a proof in some more conventional system which it then
checks in a conventional way.  However, there is no requirement that
PC  operate in this way; all we require is that when  PC(s,y)  is
true that a proof of  s  in  L  exists.

	4. Another possibility is that  y  is a program but  PC
doesn't interpret  y.  Instead  PC  and  y  operate as co-routines
engaging in a dialog wherein  y  attempts to convince  PC  that
s  is a theorem.  This has a certain neatness, but unless  PC  has
some way of bounding the time and space used by  y  we don't get
a bounded proof-checker.  I suppose  PC  could run a clock while
y  is running and require that  y  work in a previously specified
amount of memory.  This all can be done, but at the moment it
doesn't seem to have any advantages over the previous scheme, and
it seem much more problematical to formalize.

	5. We don't  suppose that  y  will normally be generated
by hand.  It will instead be generated by an interactive program  PF
that looks for a generalized proof, i.e. a suitable  y.  This program,
once the human decisions are recorded and incorporated could itself
be regarded as the  y, but ordinarily it will have pursued a number
of blind alleys.  Sometimes  y  will be a pruned version  of  PF
with as many blind alleys pruned away as can be done without
lengthening  PF  unduly.

	6. Our general object here is to provide as flexible as
possible a notion of a verification of an assertion that can be
generated by interactive programs and verified by a verification
program.  The claim that the verification is doable in a given
time and space is part of what is to be verified.